the_es:event_system{i:l}, e,e':es-E(the_es).
es-locl(the_es; e; e')
 (((es-first(the_es; e')))
  ((e = es-pred(the_es; e'))  es-locl(the_es; e; es-pred(the_es; e')))) 

latex

Definitions	x:A. B(x), t  T, P  Q, P  Q, P  Q, P  Q, A c B, P  Q, prop{i:l}, A, guard(T), False, trans(T; x,y.E(x;y))
Lemmas	es-axioms, event system wf, es-locl wf, not wf, assert wf, es-first wf, es-E wf, es-pred wf, Id wf, es-loc wf, es-loc-pred